package org.xtext.runtime.util;

import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Queue;
import java.util.Set;
import java.util.Stack;

import org.xtext.runtime.formula.AND;
import org.xtext.runtime.formula.IComparison;
import org.xtext.runtime.formula.IFormula;
import org.xtext.runtime.formula.IMPLIES;
import org.xtext.runtime.formula.NOT;
import org.xtext.runtime.formula.Predicate;
import org.xtext.runtime.formula.TRActive;
import org.xtext.runtime.term.Variable;

public class ResolutionBasedReasoner implements IReasoner {
	private static final int MAX_DEPTH 										= 20;
	private static long counter 											= 0;
	
	List<IQueryable> sources = new LinkedList<IQueryable>();
	
	Stack<IReasonerStackEntry> stack;
	Stack<IFormula> formulae;
	List<Bindings> solutions;
	boolean singleResult;

	private class TRActiveStackEntry implements IReasonerStackEntry {
		TRActive function;
		Queue<IFormula> options = new LinkedList<IFormula>();
		List<Bindings> solutions = new LinkedList<Bindings>();
		boolean solved = false;
		Bindings initial;

		public TRActiveStackEntry(TRActive function, Bindings bindings) {
			this.function = function;
			this.initial = bindings;
			
			// Generate matching formulae
			for (IQueryable source : sources) {
				List<IFormula> list = source.getMatchingFormulae(function);
				if (list != null) options.addAll(list);
			}
		}
		
		@Override
		public boolean solve() {
			if (options.isEmpty()) {
				if (solved) {
					for (Bindings bindings : solutions) {
						propagateBindings(initial.merge(bindings));
					}
				}
				stack.pop();
				return solved;
			}
			
			TRActive active = (TRActive) options.remove();
			Bindings bindings = Unifier.unify(function.formula(), active.formula());
			if (bindings != null) {
				solved = true;
				propagateBindings(initial.merge(bindings));
				if (singleResult) options.clear();
			}

			return true;
		}

		public String toString() {
			return function.toString() + " / " + options;
		}

		@Override
		public boolean failure() {
			// Do nothing, and propagate failure (this is called when a
			// predicate cannot be solved)
			return true;
		}

		@Override
		public void addBindings(Bindings bindings) {
			solutions.add(bindings);
		}
	}

	private class PredicateStackEntry implements IReasonerStackEntry {
		Predicate predicate;
		Queue<IFormula> options = new LinkedList<IFormula>();
		boolean solved = false;
		Set<Variable> freeVariables = new HashSet<Variable>();
		List<Bindings> solutions = new LinkedList<Bindings>();
		IFormula nextFormula;
		Bindings initial;
		
		public PredicateStackEntry(Predicate predicate, Bindings bindings) {
			this.predicate = predicate;
			this.initial = bindings;
			
			// Identify Free Variables
			for (Variable variable : predicate.variables()) {
				if (variable.isFree()) {
					freeVariables.add(variable);
				}
			}
			
			// Generate matching formulae
			for (IQueryable source : sources) {
				List<IFormula> list = source.getMatchingFormulae(predicate);
//				System.out.println("predicate: " + predicate + " / list: " + list);
				if (list != null) options.addAll(list);
			}
		}
		
		public boolean solve() {
			if (predicate.equals(Predicate.FALSE)) {
				stack.pop();
				return false;
			}
			if (predicate.equals(Predicate.TRUE)) {
				stack.pop();
				return true;
			}
			
			if (options.isEmpty()) {
				if (solved) {
					for (Bindings bindings : solutions) {
						propagateBindings(initial.merge(bindings));
					}
				}
				stack.pop();
				return solved;
			}
			
			nextFormula = options.remove();
			if (Predicate.class.isInstance(nextFormula)) {
				Bindings bindings = Unifier.unify(predicate, (Predicate) nextFormula);
				if (bindings != null) {
					solved = true;
//					System.out.println("bindings: " + bindings);
					propagateBindings(initial.merge(bindings));
					if (singleResult) options.clear();
//				} else {
//					System.out.println("No unification: " + predicate + " / " + nextFormula);
				}
			} else if (IMPLIES.class.isInstance(nextFormula)) {
				IMPLIES implies = (IMPLIES) nextFormula;
				implies = implies.rename("rn_" + (counter++) + "_");
				Bindings bindings = Unifier.unify(predicate, implies.result());
				if (bindings != null) {
					solved = true;

					stack.push(newStackEntry(implies.context(), bindings.copy()));
					if (singleResult) options.clear();
				}
			}

			for (Variable variable : freeVariables) {
				variable.clear();
			}
			
			return true;
		}

		public String toString() {
			return predicate.toString() + " / " + options;
		}

		@Override
		public boolean failure() {
			// Do nothing, and propagate failure (this is called when a
			// predicate cannot be solved)
			return true;
		}

		@Override
		public void addBindings(Bindings bindings) {
			solutions.add(bindings);
		}
	}
	
	private class NOTStackEntry implements IReasonerStackEntry {
		NOT not;
		boolean handled = false;
		boolean sr;
		boolean failed = false;
		Bindings bindings;
		
		public NOTStackEntry(NOT not, Bindings bindings) {
			this.not = not;
			this.bindings = bindings;
		}
		
		@Override
		public boolean solve() {
			if (!handled) {
				stack.push(newStackEntry(not.formula(), bindings));
				handled = true;
				sr = singleResult;
				singleResult = true;
			} else {
				if (!failed) {
//					System.out.println("failed...");
					stack.pop();
					// This means that the enclosed formula is true, so its
					// negation must be false...
					return false;
				}
//				System.out.println("propgating: "+  bindings);
				propagateBindings(bindings);
				stack.pop();
			}
			return true;
		}

		public String toString() {
			return not.toString();
		}

		@Override
		public boolean failure() {
			// The enclosed formula could not be solved, so its negation
			// is true :o)
			// rest single result to whatever it was before the not was called
			// (this is because negation requires only to find a solution for
			// the enclosed formula)
			singleResult = sr;
			failed = true;
			return false;
		}

		@Override
		public void addBindings(Bindings bindings) {
			// Think about what to do here...
		}
	}
	
	private class ComparisonStackEntry implements IReasonerStackEntry {
		IComparison comparison;
		Bindings bindings;
		
		public ComparisonStackEntry(IComparison evaluable, Bindings bindings) {
			this.comparison = evaluable;
			this.bindings = bindings;
		}
		
		@Override
		public boolean solve() {
			boolean result = comparison.evaluate();
			if (result) {
				propagateBindings(bindings);
			}
			stack.pop();
			return result;
		}

		public String toString() {
			return comparison.toString();
		}

		@Override
		public boolean failure() {
			// This should not be called (it is a leaf node)
			return false;
		}

		@Override
		public void addBindings(Bindings bindings) {
			// This should not be called (it is a leaf node)
		}
	}
	
	private class ANDStackEntry implements IReasonerStackEntry {
		AND and;
		int index = 0;
		Queue<Bindings> queue = new LinkedList<Bindings>();
		Queue<Bindings> next = new LinkedList<Bindings>();
		Bindings bindings;
		List<Bindings> solutions = new LinkedList<Bindings>();
		
		public ANDStackEntry(AND and, Bindings bindings) {
			this.and = and;
			queue.add(bindings);
		}
		
		@Override
		public boolean solve() {
			if (index < and.formulae().length) {
				if (!queue.isEmpty()) {
					bindings = queue.remove();
					try {
						stack.push(newStackEntry(and.formulae()[index].copy().apply(bindings), bindings));
					} catch (NullPointerException e) {
						System.err.println("Formula: " + and.formulae()[index]);
						e.printStackTrace();
					}
				} else {
					queue = next;
					next = new LinkedList<Bindings>();
					index++;
				}
			} else {
//				System.out.println("at end of query..." + solutions);
				while (!solutions.isEmpty()) {
//					propagateBindings(initial.merge(queue.remove()));
					propagateBindings(solutions.remove(0));
				}
				stack.pop();
			}
			
			return true;
		}

		public String toString() {
			return and.toString();
		}

		@Override
		public boolean failure() {
			// If a single formula is false, then the AND formula is
			// false...
			if (queue.isEmpty()) {
//				System.out.println("No more solutions");
				return true;
			}
			
//			System.out.println("More solutions to handle...");
			return false;
		}

		@Override
		public void addBindings(Bindings bindings) {
			if (index < and.formulae().length-1) {
//				System.out.println("adding to next:"  + bindings);
				next.add(bindings);
			} else {
//				System.out.println("adding to solutions:"  + bindings);
				solutions.add(bindings);
			}
		}
	}
	
	private void propagateBindings(Bindings bindings) {
		if (stack.size() == 1) {
//			System.out.println("Adding to solutions: " + bindings);
			solutions.add(bindings);
		} else {
//			System.out.println("adding: " + bindings + " to: " + stack.get(stack.size()-2).getClass().getCanonicalName());
			stack.get(stack.size()-2).addBindings(bindings);
		}
	}

	private IReasonerStackEntry newStackEntry(IFormula formula, Bindings bindings) {
		IReasonerStackEntry entry = null;
		if (Predicate.class.isInstance(formula)) {
			entry = new PredicateStackEntry((Predicate) formula, bindings);
		} else if (NOT.class.isInstance(formula)) {
			entry = new NOTStackEntry((NOT) formula, bindings);
		} else if (IComparison.class.isInstance(formula)) {
			entry = new ComparisonStackEntry((IComparison) formula, bindings);
		} else if (AND.class.isInstance(formula)) {
			entry = new ANDStackEntry((AND) formula, bindings);
		} else if (TRActive.class.isInstance(formula)) {
			entry = new TRActiveStackEntry((TRActive) formula, bindings);
		} else {
			System.err.println("Reasoner did not handle entry: " + formula);
			return null;
		}
		
		return entry;
	}
	
	public void addSource(IQueryable source) {
		sources.add(source);
	}
	
	public List<Bindings> queryAll(IFormula formula) {
		this.singleResult = false;
		return doQuery(formula);
	}
	
	public List<Bindings> query(IFormula formula) {
//		System.out.println("formula: " +formula);
		this.singleResult = true;
		return doQuery(formula);
	}
	
	private List<Bindings> doQuery(IFormula formula) {
		stack = new Stack<IReasonerStackEntry>();
		formulae = new Stack<IFormula>();
		solutions = new LinkedList<Bindings>();

//		System.out.println("[resolutionbasedreasoner] formula: " + formula);
		stack.push(newStackEntry(formula.copy(), new Bindings()));
		while (!stack.isEmpty() && stack.size() < MAX_DEPTH) {
//			System.out.println("stack: " + stack.peek().toString() + " / " + stack.size());
			if (!stack.peek().solve()) {
				if (!propogateFailure()) return null;
			}
		}
		
//		System.out.println("solutions: " + solutions);
//		System.out.println(formula.variables());
		// Remove redundant bindings..
		List<Bindings> filtered = new LinkedList<Bindings>();
		for (Bindings bindings : solutions) {
			try {
				filtered.add(bindings.filter(formula.variables()));
			} catch (BindingException e) {
				// Ignore: This happens when a variable is introduced in a negated formula
				// i.e. there is no X such that the formula is true...
				e.printStackTrace();
			}
		}
		return filtered;
	}
	
	private boolean propogateFailure() {
		while (!stack.isEmpty() && stack.peek().failure()) stack.pop();

//		System.out.println("stack size: " + stack.size());
		return !stack.isEmpty();
	}
}
